minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
↳ QTRS
↳ Overlay + Local Confluence
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
MOD(x, s(y)) → LT(x, s(y))
IF1(false, x, y) → MOD(minus(x, y), y)
IF1(false, x, y) → MINUS(x, y)
GT(s(x), s(y)) → GT(x, y)
LT(s(x), s(y)) → LT(x, y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
MOD(x, s(y)) → LT(x, s(y))
IF1(false, x, y) → MOD(minus(x, y), y)
IF1(false, x, y) → MINUS(x, y)
GT(s(x), s(y)) → GT(x, y)
LT(s(x), s(y)) → LT(x, y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
LT(s(x), s(y)) → LT(x, y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
LT(s(x), s(y)) → LT(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
LT(s(x), s(y)) → LT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
IF1(false, x, y) → MOD(minus(x, y), y)
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
mod(x, 0) → 0
mod(x, s(y)) → if1(lt(x, s(y)), x, s(y))
if1(true, x, y) → x
if1(false, x, y) → mod(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
lt(x, 0) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF1(false, x, y) → MOD(minus(x, y), y)
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
IF1(false, x, y) → MOD(minus(x, y), y)
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
IF1(false, z0, s(z1)) → MOD(minus(z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Narrowing
MOD(x, s(y)) → IF1(lt(x, s(y)), x, s(y))
IF1(false, z0, s(z1)) → MOD(minus(z0, s(z1)), s(z1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
MOD(0, s(x0)) → IF1(true, 0, s(x0))
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
IF1(false, x, y) → MOD(minus(x, y), y)
MOD(0, s(x0)) → IF1(true, 0, s(x0))
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
IF1(false, x, y) → MOD(minus(x, y), y)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
IF1(false, 0, x0) → MOD(0, x0)
IF1(false, s(x0), x1) → MOD(if(gt(s(x0), x1), x0, x1), x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
IF1(false, 0, x0) → MOD(0, x0)
IF1(false, s(x0), x1) → MOD(if(gt(s(x0), x1), x0, x1), x1)
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
IF1(false, s(x0), x1) → MOD(if(gt(s(x0), x1), x0, x1), x1)
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
IF1(false, s(z0), s(z1)) → MOD(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
IF1(false, s(z0), s(z1)) → MOD(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
IF1(false, s(z0), s(z1)) → MOD(if(gt(z0, z1), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
IF1(false, s(z0), s(z1)) → MOD(if(gt(z0, z1), z0, s(z1)), s(z1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
POL(0) = 0
POL(IF1(x1, x2, x3)) = x1 + x2
POL(MOD(x1, x2)) = 1 + x1
POL(false) = 1
POL(gt(x1, x2)) = 1
POL(if(x1, x2, x3)) = 1 + x2
POL(lt(x1, x2)) = 1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QTRS
MOD(s(x0), s(x1)) → IF1(lt(x0, x1), s(x0), s(x1))
minus(0, y) → 0
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gt(0, y) → false
lt(0, s(x)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false
minus(0, x0)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
minus'(0, y3) → false
minus'(s(x13), y11) → if'(gt(s(x13), y11), x13, y11)
if'(true, x32, y27) → minus'(x32, y27)
if'(false, x41, y35) → true
gt(s(x'), 0) → true
minus(0, y3) → 0
minus(s(x13), y11) → if(gt(s(x13), y11), x13, y11)
gt(s(x23), s(y19)) → gt(x23, y19)
if(true, x32, y27) → s(minus(x32, y27))
if(false, x41, y35) → 0
gt(0, y43) → false
lt(0, s(x58)) → true
lt(s(x67), s(y58)) → lt(x67, y58)
lt(x76, 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
minus'(0, y3) → false
minus'(s(x13), y11) → if'(gt(s(x13), y11), x13, y11)
if'(true, x32, y27) → minus'(x32, y27)
if'(false, x41, y35) → true
gt(s(x'), 0) → true
minus(0, y3) → 0
minus(s(x13), y11) → if(gt(s(x13), y11), x13, y11)
gt(s(x23), s(y19)) → gt(x23, y19)
if(true, x32, y27) → s(minus(x32, y27))
if(false, x41, y35) → 0
gt(0, y43) → false
lt(0, s(x58)) → true
lt(s(x67), s(y58)) → lt(x67, y58)
lt(x76, 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
[minus'2, 0, false, if'3, not1, isafalse1] > [true, minus2, if3, equalsort[a0]2] > s1
[minus'2, 0, false, if'3, not1, isafalse1] > [true, minus2, if3, equalsort[a0]2] > gt2
equalsort[a39]2 > [true, minus2, if3, equalsort[a0]2] > s1
equalsort[a39]2 > [true, minus2, if3, equalsort[a0]2] > gt2
minus2: [1,2]
minus'2: [1,2]
true: multiset
or2: multiset
and2: multiset
gt2: multiset
0: multiset
equalbool2: [2,1]
equalsort[a0]2: multiset
equalsort[a39]2: multiset
if3: [2,3,1]
if'3: [2,3,1]
not1: multiset
witnesssort[a39]: multiset
isafalse1: multiset
false: multiset
s1: multiset
lt2: [2,1]
isatrue1: multiset
minus'(0, y3) → false
minus'(s(x13), y11) → if'(gt(s(x13), y11), x13, y11)
if'(true, x32, y27) → minus'(x32, y27)
if'(false, x41, y35) → true
gt(s(x'), 0) → true
minus(0, y3) → 0
minus(s(x13), y11) → if(gt(s(x13), y11), x13, y11)
gt(s(x23), s(y19)) → gt(x23, y19)
if(true, x32, y27) → s(minus(x32, y27))
if(false, x41, y35) → 0
gt(0, y43) → false
lt(0, s(x58)) → true
lt(s(x67), s(y58)) → lt(x67, y58)
lt(x76, 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof